1. $A$ : Type
\\[0ex]2. $e$ : $A$
\\[0ex]3. $H$ : $A$$\rightarrow$Type
\\[0ex]4. $\exists$$x$:$A$. ($e$ = $x$)
\\[0ex]5. $z$ : $H$($e$)
\\[0ex]6. $A$ $\in$ Type
\\[0ex]7. $e$ $\in$ $A$
\\[0ex]8. $\forall$$x$:$A$. ($e$ = $x$) $\in$ Type
\\[0ex]$\vdash$  $z$ $\neq$ 0